Nuprl Lemma : singleton-subtype
11,40
postcript
pdf
A
,
B
:Type. strong-subtype(
A
;
B
)
(
a
:
A
. {
z
:
B
|
z
=
a
B
}
r
A
)
latex
Definitions
{
x
:
A
|
B
(
x
)}
,
x
:
A
.
B
(
x
)
,
s
=
t
,
(
x
l
)
,
x
.
t
(
x
)
,
,
<
a
,
b
>
,
type
List
,
P
Q
,
P
&
Q
,
P
Q
,
left
+
right
,
,
A
c
B
,
t
T
,
Type
,
x
:
A
B
(
x
)
,
P
Q
,
strong-subtype(
A
;
B
)
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
Lemmas
subtype
rel
wf
,
subtype
rel
transitivity
,
member
wf
,
subtype
rel
set
origin
A, B:Type. strong-subtype(A;B) 
(a:A. {z:B| z = a 
B} 
r A) A, B:Type. strong-subtype(A;B) (a:A. {z:B| z = a B} r A) 
x:A. B(x) l)
x. t(x)
Q Q
B T
B(x) Qx:A. B(x)
B(x)